Nuprl Definition : rel-immediate
11,40
postcript
pdf
rel-immediate(
T
;
R
)(
x
,
y
) == (
R
(
x
,
y
))
(
z
:
T
.
((
R
(
x
,
z
))
(
R
(
z
,
y
))))
latex
Definitions
x
.
A
(
x
)
,
x
:
A
.
B
(
x
)
,
A
,
P
Q
,
f
(
a
)
FDL editor aliases
rel-immediate
origin
(
z:T. 
((R(x,z)) (R(z,y)))) (z:T. ((R(x,z)) (R(z,y)))) 
x.A(x)x:A. B(x)A Q